Lean 4 > Mathlibから圏を見る
code:lean
class Category (obj : Type u) : Type max u (v + 1) extends CategoryStruct.{v} obj where
対象はType u
code:lean
-- 定義全体
/-- The typeclass Category C describes morphisms associated to objects of type C.
The universe levels of the objects and morphisms are unconstrained, and will often need to be
specified explicitly, as Category.{v} C. (See also LargeCategory and SmallCategory.) -/
class Category (obj : Type u) : Type max u (v + 1) extends CategoryStruct.{v} obj where
/-- Identity morphisms are left identities for composition. -/
id_comp : ∀ {X Y : obj} (f : X ⟶ Y), 𝟙 X ≫ f = f := by aesop_cat
/-- Identity morphisms are right identities for composition. -/
comp_id : ∀ {X Y : obj} (f : X ⟶ Y), f ≫ 𝟙 Y = f := by aesop_cat
/-- Composition in a category is associative. -/
assoc : ∀ {W X Y Z : obj} (f : W ⟶ X) (g : X ⟶ Y) (h : Y ⟶ Z), (f ≫ g) ≫ h = f ≫ g ≫ h := by
aesop_cat
code:lean
class CategoryStruct (obj : Type u) : Type max u (v + 1) extends Quiver.{v + 1} obj where
code:lean
/-- A preliminary structure on the way to defining a category,
containing the data, but none of the axioms. -/
class CategoryStruct (obj : Type u) : Type max u (v + 1) extends Quiver.{v + 1} obj where
/-- The identity morphism on an object. -/
id : ∀ X : obj, Hom X X
/-- Composition of morphisms in a category, written f ≫ g. -/
comp : ∀ {X Y Z : obj}, (X ⟶ Y) → (Y ⟶ Z) → (X ⟶ Z)
code:lean
/-- A quiver G on a type V of vertices assigns to every pair a b : V of vertices
a type a ⟶ b of arrows from a to b.
For graphs with no repeated edges, one can use Quiver.{0} V, which ensures
a ⟶ b : Prop. For multigraphs, one can use Quiver.{v+1} V, which ensures
a ⟶ b : Type v.
Because Category will later extend this class, we call the field Hom.
Except when constructing instances, you should rarely see this, and use the ⟶ notation instead.
-/
class Quiver (V : Type u) where
/-- The type of edges/arrows/morphisms between a given source and target. -/
Hom : V → V → Sort v
対象は(obj : Type u) : Type max u (v + 1)